Termination w.r.t. Q proof of TRS/Cimelse.trs

Termination w.r.t. Q of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

Term_sub₂(Case₃(m, xi, n), s) -> Frozen₄(m, Sum_sub₂(xi, s), n, s)
Frozen₄(m, Sum_constant₁(Left), n, s) -> Term_sub₂(m, s)
Frozen₄(m, Sum_constant₁(Right), n, s) -> Term_sub₂(n, s)
Frozen₄(m, Sum_term_var₁(xi), n, s) -> Case₃(Term_sub₂(m, s), xi, Term_sub₂(n, s))
Term_sub₂(Term_app₂(m, n), s) -> Term_app₂(Term_sub₂(m, s), Term_sub₂(n, s))
Term_sub₂(Term_pair₂(m, n), s) -> Term_pair₂(Term_sub₂(m, s), Term_sub₂(n, s))
Term_sub₂(Term_inl₁(m), s) -> Term_inl₁(Term_sub₂(m, s))
Term_sub₂(Term_inr₁(m), s) -> Term_inr₁(Term_sub₂(m, s))
Term_sub₂(Term_var₁(x), Id) -> Term_var₁(x)
Term_sub₂(Term_var₁(x), Cons_usual₃(y, m, s)) -> m
Term_sub₂(Term_var₁(x), Cons_usual₃(y, m, s)) -> Term_sub₂(Term_var₁(x), s)
Term_sub₂(Term_var₁(x), Cons_sum₃(xi, k, s)) -> Term_sub₂(Term_var₁(x), s)
Term_sub₂(Term_sub₂(m, s), t) -> Term_sub₂(m, Concat₂(s, t))
Sum_sub₂(xi, Id) -> Sum_term_var₁(xi)
Sum_sub₂(xi, Cons_sum₃(psi, k, s)) -> Sum_constant₁(k)
Sum_sub₂(xi, Cons_sum₃(psi, k, s)) -> Sum_sub₂(xi, s)
Sum_sub₂(xi, Cons_usual₃(y, m, s)) -> Sum_sub₂(xi, s)
Concat₂(Concat₂(s, t), u) -> Concat₂(s, Concat₂(t, u))
Concat₂(Cons_usual₃(x, m, s), t) -> Cons_usual₃(x, Term_sub₂(m, t), Concat₂(s, t))
Concat₂(Cons_sum₃(xi, k, s), t) -> Cons_sum₃(xi, k, Concat₂(s, t))
Concat₂(Id, s) -> s

Q is empty.

↳ QTRS

  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

Term_sub₂(Case₃(m, xi, n), s) -> Frozen₄(m, Sum_sub₂(xi, s), n, s)
Frozen₄(m, Sum_constant₁(Left), n, s) -> Term_sub₂(m, s)
Frozen₄(m, Sum_constant₁(Right), n, s) -> Term_sub₂(n, s)
Frozen₄(m, Sum_term_var₁(xi), n, s) -> Case₃(Term_sub₂(m, s), xi, Term_sub₂(n, s))
Term_sub₂(Term_app₂(m, n), s) -> Term_app₂(Term_sub₂(m, s), Term_sub₂(n, s))
Term_sub₂(Term_pair₂(m, n), s) -> Term_pair₂(Term_sub₂(m, s), Term_sub₂(n, s))
Term_sub₂(Term_inl₁(m), s) -> Term_inl₁(Term_sub₂(m, s))
Term_sub₂(Term_inr₁(m), s) -> Term_inr₁(Term_sub₂(m, s))
Term_sub₂(Term_var₁(x), Id) -> Term_var₁(x)
Term_sub₂(Term_var₁(x), Cons_usual₃(y, m, s)) -> m
Term_sub₂(Term_var₁(x), Cons_usual₃(y, m, s)) -> Term_sub₂(Term_var₁(x), s)
Term_sub₂(Term_var₁(x), Cons_sum₃(xi, k, s)) -> Term_sub₂(Term_var₁(x), s)
Term_sub₂(Term_sub₂(m, s), t) -> Term_sub₂(m, Concat₂(s, t))
Sum_sub₂(xi, Id) -> Sum_term_var₁(xi)
Sum_sub₂(xi, Cons_sum₃(psi, k, s)) -> Sum_constant₁(k)
Sum_sub₂(xi, Cons_sum₃(psi, k, s)) -> Sum_sub₂(xi, s)
Sum_sub₂(xi, Cons_usual₃(y, m, s)) -> Sum_sub₂(xi, s)
Concat₂(Concat₂(s, t), u) -> Concat₂(s, Concat₂(t, u))
Concat₂(Cons_usual₃(x, m, s), t) -> Cons_usual₃(x, Term_sub₂(m, t), Concat₂(s, t))
Concat₂(Cons_sum₃(xi, k, s), t) -> Cons_sum₃(xi, k, Concat₂(s, t))
Concat₂(Id, s) -> s

Q is empty.

Using Dependency Pairs [1,13] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

TERM_SUB₂(Term_sub₂(m, s), t) -> CONCAT₂(s, t)
TERM_SUB₂(Term_sub₂(m, s), t) -> TERM_SUB₂(m, Concat₂(s, t))
TERM_SUB₂(Case₃(m, xi, n), s) -> FROZEN₄(m, Sum_sub₂(xi, s), n, s)
TERM_SUB₂(Term_inl₁(m), s) -> TERM_SUB₂(m, s)
TERM_SUB₂(Term_var₁(x), Cons_usual₃(y, m, s)) -> TERM_SUB₂(Term_var₁(x), s)
CONCAT₂(Cons_usual₃(x, m, s), t) -> CONCAT₂(s, t)
CONCAT₂(Concat₂(s, t), u) -> CONCAT₂(s, Concat₂(t, u))
CONCAT₂(Cons_usual₃(x, m, s), t) -> TERM_SUB₂(m, t)
TERM_SUB₂(Term_app₂(m, n), s) -> TERM_SUB₂(n, s)
TERM_SUB₂(Case₃(m, xi, n), s) -> SUM_SUB₂(xi, s)
FROZEN₄(m, Sum_constant₁(Right), n, s) -> TERM_SUB₂(n, s)
CONCAT₂(Concat₂(s, t), u) -> CONCAT₂(t, u)
TERM_SUB₂(Term_pair₂(m, n), s) -> TERM_SUB₂(n, s)
TERM_SUB₂(Term_inr₁(m), s) -> TERM_SUB₂(m, s)
FROZEN₄(m, Sum_constant₁(Left), n, s) -> TERM_SUB₂(m, s)
SUM_SUB₂(xi, Cons_sum₃(psi, k, s)) -> SUM_SUB₂(xi, s)
TERM_SUB₂(Term_app₂(m, n), s) -> TERM_SUB₂(m, s)
FROZEN₄(m, Sum_term_var₁(xi), n, s) -> TERM_SUB₂(n, s)
SUM_SUB₂(xi, Cons_usual₃(y, m, s)) -> SUM_SUB₂(xi, s)
TERM_SUB₂(Term_var₁(x), Cons_sum₃(xi, k, s)) -> TERM_SUB₂(Term_var₁(x), s)
FROZEN₄(m, Sum_term_var₁(xi), n, s) -> TERM_SUB₂(m, s)
CONCAT₂(Cons_sum₃(xi, k, s), t) -> CONCAT₂(s, t)
TERM_SUB₂(Term_pair₂(m, n), s) -> TERM_SUB₂(m, s)

The TRS R consists of the following rules:

Term_sub₂(Case₃(m, xi, n), s) -> Frozen₄(m, Sum_sub₂(xi, s), n, s)
Frozen₄(m, Sum_constant₁(Left), n, s) -> Term_sub₂(m, s)
Frozen₄(m, Sum_constant₁(Right), n, s) -> Term_sub₂(n, s)
Frozen₄(m, Sum_term_var₁(xi), n, s) -> Case₃(Term_sub₂(m, s), xi, Term_sub₂(n, s))
Term_sub₂(Term_app₂(m, n), s) -> Term_app₂(Term_sub₂(m, s), Term_sub₂(n, s))
Term_sub₂(Term_pair₂(m, n), s) -> Term_pair₂(Term_sub₂(m, s), Term_sub₂(n, s))
Term_sub₂(Term_inl₁(m), s) -> Term_inl₁(Term_sub₂(m, s))
Term_sub₂(Term_inr₁(m), s) -> Term_inr₁(Term_sub₂(m, s))
Term_sub₂(Term_var₁(x), Id) -> Term_var₁(x)
Term_sub₂(Term_var₁(x), Cons_usual₃(y, m, s)) -> m
Term_sub₂(Term_var₁(x), Cons_usual₃(y, m, s)) -> Term_sub₂(Term_var₁(x), s)
Term_sub₂(Term_var₁(x), Cons_sum₃(xi, k, s)) -> Term_sub₂(Term_var₁(x), s)
Term_sub₂(Term_sub₂(m, s), t) -> Term_sub₂(m, Concat₂(s, t))
Sum_sub₂(xi, Id) -> Sum_term_var₁(xi)
Sum_sub₂(xi, Cons_sum₃(psi, k, s)) -> Sum_constant₁(k)
Sum_sub₂(xi, Cons_sum₃(psi, k, s)) -> Sum_sub₂(xi, s)
Sum_sub₂(xi, Cons_usual₃(y, m, s)) -> Sum_sub₂(xi, s)
Concat₂(Concat₂(s, t), u) -> Concat₂(s, Concat₂(t, u))
Concat₂(Cons_usual₃(x, m, s), t) -> Cons_usual₃(x, Term_sub₂(m, t), Concat₂(s, t))
Concat₂(Cons_sum₃(xi, k, s), t) -> Cons_sum₃(xi, k, Concat₂(s, t))
Concat₂(Id, s) -> s

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

TERM_SUB₂(Term_sub₂(m, s), t) -> CONCAT₂(s, t)
TERM_SUB₂(Term_sub₂(m, s), t) -> TERM_SUB₂(m, Concat₂(s, t))
TERM_SUB₂(Case₃(m, xi, n), s) -> FROZEN₄(m, Sum_sub₂(xi, s), n, s)
TERM_SUB₂(Term_inl₁(m), s) -> TERM_SUB₂(m, s)
TERM_SUB₂(Term_var₁(x), Cons_usual₃(y, m, s)) -> TERM_SUB₂(Term_var₁(x), s)
CONCAT₂(Cons_usual₃(x, m, s), t) -> CONCAT₂(s, t)
CONCAT₂(Concat₂(s, t), u) -> CONCAT₂(s, Concat₂(t, u))
CONCAT₂(Cons_usual₃(x, m, s), t) -> TERM_SUB₂(m, t)
TERM_SUB₂(Term_app₂(m, n), s) -> TERM_SUB₂(n, s)
TERM_SUB₂(Case₃(m, xi, n), s) -> SUM_SUB₂(xi, s)
FROZEN₄(m, Sum_constant₁(Right), n, s) -> TERM_SUB₂(n, s)
CONCAT₂(Concat₂(s, t), u) -> CONCAT₂(t, u)
TERM_SUB₂(Term_pair₂(m, n), s) -> TERM_SUB₂(n, s)
TERM_SUB₂(Term_inr₁(m), s) -> TERM_SUB₂(m, s)
FROZEN₄(m, Sum_constant₁(Left), n, s) -> TERM_SUB₂(m, s)
SUM_SUB₂(xi, Cons_sum₃(psi, k, s)) -> SUM_SUB₂(xi, s)
TERM_SUB₂(Term_app₂(m, n), s) -> TERM_SUB₂(m, s)
FROZEN₄(m, Sum_term_var₁(xi), n, s) -> TERM_SUB₂(n, s)
SUM_SUB₂(xi, Cons_usual₃(y, m, s)) -> SUM_SUB₂(xi, s)
TERM_SUB₂(Term_var₁(x), Cons_sum₃(xi, k, s)) -> TERM_SUB₂(Term_var₁(x), s)
FROZEN₄(m, Sum_term_var₁(xi), n, s) -> TERM_SUB₂(m, s)
CONCAT₂(Cons_sum₃(xi, k, s), t) -> CONCAT₂(s, t)
TERM_SUB₂(Term_pair₂(m, n), s) -> TERM_SUB₂(m, s)

The TRS R consists of the following rules:

Term_sub₂(Case₃(m, xi, n), s) -> Frozen₄(m, Sum_sub₂(xi, s), n, s)
Frozen₄(m, Sum_constant₁(Left), n, s) -> Term_sub₂(m, s)
Frozen₄(m, Sum_constant₁(Right), n, s) -> Term_sub₂(n, s)
Frozen₄(m, Sum_term_var₁(xi), n, s) -> Case₃(Term_sub₂(m, s), xi, Term_sub₂(n, s))
Term_sub₂(Term_app₂(m, n), s) -> Term_app₂(Term_sub₂(m, s), Term_sub₂(n, s))
Term_sub₂(Term_pair₂(m, n), s) -> Term_pair₂(Term_sub₂(m, s), Term_sub₂(n, s))
Term_sub₂(Term_inl₁(m), s) -> Term_inl₁(Term_sub₂(m, s))
Term_sub₂(Term_inr₁(m), s) -> Term_inr₁(Term_sub₂(m, s))
Term_sub₂(Term_var₁(x), Id) -> Term_var₁(x)
Term_sub₂(Term_var₁(x), Cons_usual₃(y, m, s)) -> m
Term_sub₂(Term_var₁(x), Cons_usual₃(y, m, s)) -> Term_sub₂(Term_var₁(x), s)
Term_sub₂(Term_var₁(x), Cons_sum₃(xi, k, s)) -> Term_sub₂(Term_var₁(x), s)
Term_sub₂(Term_sub₂(m, s), t) -> Term_sub₂(m, Concat₂(s, t))
Sum_sub₂(xi, Id) -> Sum_term_var₁(xi)
Sum_sub₂(xi, Cons_sum₃(psi, k, s)) -> Sum_constant₁(k)
Sum_sub₂(xi, Cons_sum₃(psi, k, s)) -> Sum_sub₂(xi, s)
Sum_sub₂(xi, Cons_usual₃(y, m, s)) -> Sum_sub₂(xi, s)
Concat₂(Concat₂(s, t), u) -> Concat₂(s, Concat₂(t, u))
Concat₂(Cons_usual₃(x, m, s), t) -> Cons_usual₃(x, Term_sub₂(m, t), Concat₂(s, t))
Concat₂(Cons_sum₃(xi, k, s), t) -> Cons_sum₃(xi, k, Concat₂(s, t))
Concat₂(Id, s) -> s

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 3 SCCs with 1 less node.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ QDPOrderProof

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

SUM_SUB₂(xi, Cons_sum₃(psi, k, s)) -> SUM_SUB₂(xi, s)
SUM_SUB₂(xi, Cons_usual₃(y, m, s)) -> SUM_SUB₂(xi, s)

The TRS R consists of the following rules:

Term_sub₂(Case₃(m, xi, n), s) -> Frozen₄(m, Sum_sub₂(xi, s), n, s)
Frozen₄(m, Sum_constant₁(Left), n, s) -> Term_sub₂(m, s)
Frozen₄(m, Sum_constant₁(Right), n, s) -> Term_sub₂(n, s)
Frozen₄(m, Sum_term_var₁(xi), n, s) -> Case₃(Term_sub₂(m, s), xi, Term_sub₂(n, s))
Term_sub₂(Term_app₂(m, n), s) -> Term_app₂(Term_sub₂(m, s), Term_sub₂(n, s))
Term_sub₂(Term_pair₂(m, n), s) -> Term_pair₂(Term_sub₂(m, s), Term_sub₂(n, s))
Term_sub₂(Term_inl₁(m), s) -> Term_inl₁(Term_sub₂(m, s))
Term_sub₂(Term_inr₁(m), s) -> Term_inr₁(Term_sub₂(m, s))
Term_sub₂(Term_var₁(x), Id) -> Term_var₁(x)
Term_sub₂(Term_var₁(x), Cons_usual₃(y, m, s)) -> m
Term_sub₂(Term_var₁(x), Cons_usual₃(y, m, s)) -> Term_sub₂(Term_var₁(x), s)
Term_sub₂(Term_var₁(x), Cons_sum₃(xi, k, s)) -> Term_sub₂(Term_var₁(x), s)
Term_sub₂(Term_sub₂(m, s), t) -> Term_sub₂(m, Concat₂(s, t))
Sum_sub₂(xi, Id) -> Sum_term_var₁(xi)
Sum_sub₂(xi, Cons_sum₃(psi, k, s)) -> Sum_constant₁(k)
Sum_sub₂(xi, Cons_sum₃(psi, k, s)) -> Sum_sub₂(xi, s)
Sum_sub₂(xi, Cons_usual₃(y, m, s)) -> Sum_sub₂(xi, s)
Concat₂(Concat₂(s, t), u) -> Concat₂(s, Concat₂(t, u))
Concat₂(Cons_usual₃(x, m, s), t) -> Cons_usual₃(x, Term_sub₂(m, t), Concat₂(s, t))
Concat₂(Cons_sum₃(xi, k, s), t) -> Cons_sum₃(xi, k, Concat₂(s, t))
Concat₂(Id, s) -> s

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

SUM_SUB₂(xi, Cons_usual₃(y, m, s)) -> SUM_SUB₂(xi, s)

The remaining pairs can at least be oriented weakly.

SUM_SUB₂(xi, Cons_sum₃(psi, k, s)) -> SUM_SUB₂(xi, s)

Used ordering: Polynomial interpretation [21]:

POL(Cons_sum₃(x₁, x₂, x₃)) = 2·x₃
POL(Cons_usual₃(x₁, x₂, x₃)) = 2 + 2·x₃
POL(SUM_SUB₂(x₁, x₂)) = 2·x₂

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ QDPOrderProof

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

SUM_SUB₂(xi, Cons_sum₃(psi, k, s)) -> SUM_SUB₂(xi, s)

The TRS R consists of the following rules:

Term_sub₂(Case₃(m, xi, n), s) -> Frozen₄(m, Sum_sub₂(xi, s), n, s)
Frozen₄(m, Sum_constant₁(Left), n, s) -> Term_sub₂(m, s)
Frozen₄(m, Sum_constant₁(Right), n, s) -> Term_sub₂(n, s)
Frozen₄(m, Sum_term_var₁(xi), n, s) -> Case₃(Term_sub₂(m, s), xi, Term_sub₂(n, s))
Term_sub₂(Term_app₂(m, n), s) -> Term_app₂(Term_sub₂(m, s), Term_sub₂(n, s))
Term_sub₂(Term_pair₂(m, n), s) -> Term_pair₂(Term_sub₂(m, s), Term_sub₂(n, s))
Term_sub₂(Term_inl₁(m), s) -> Term_inl₁(Term_sub₂(m, s))
Term_sub₂(Term_inr₁(m), s) -> Term_inr₁(Term_sub₂(m, s))
Term_sub₂(Term_var₁(x), Id) -> Term_var₁(x)
Term_sub₂(Term_var₁(x), Cons_usual₃(y, m, s)) -> m
Term_sub₂(Term_var₁(x), Cons_usual₃(y, m, s)) -> Term_sub₂(Term_var₁(x), s)
Term_sub₂(Term_var₁(x), Cons_sum₃(xi, k, s)) -> Term_sub₂(Term_var₁(x), s)
Term_sub₂(Term_sub₂(m, s), t) -> Term_sub₂(m, Concat₂(s, t))
Sum_sub₂(xi, Id) -> Sum_term_var₁(xi)
Sum_sub₂(xi, Cons_sum₃(psi, k, s)) -> Sum_constant₁(k)
Sum_sub₂(xi, Cons_sum₃(psi, k, s)) -> Sum_sub₂(xi, s)
Sum_sub₂(xi, Cons_usual₃(y, m, s)) -> Sum_sub₂(xi, s)
Concat₂(Concat₂(s, t), u) -> Concat₂(s, Concat₂(t, u))
Concat₂(Cons_usual₃(x, m, s), t) -> Cons_usual₃(x, Term_sub₂(m, t), Concat₂(s, t))
Concat₂(Cons_sum₃(xi, k, s), t) -> Cons_sum₃(xi, k, Concat₂(s, t))
Concat₂(Id, s) -> s

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

SUM_SUB₂(xi, Cons_sum₃(psi, k, s)) -> SUM_SUB₂(xi, s)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [21]:

POL(Cons_sum₃(x₁, x₂, x₃)) = 1 + 2·x₃
POL(SUM_SUB₂(x₁, x₂)) = 2·x₂

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

                    ↳ PisEmptyProof

          ↳ QDP

          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

Term_sub₂(Case₃(m, xi, n), s) -> Frozen₄(m, Sum_sub₂(xi, s), n, s)
Frozen₄(m, Sum_constant₁(Left), n, s) -> Term_sub₂(m, s)
Frozen₄(m, Sum_constant₁(Right), n, s) -> Term_sub₂(n, s)
Frozen₄(m, Sum_term_var₁(xi), n, s) -> Case₃(Term_sub₂(m, s), xi, Term_sub₂(n, s))
Term_sub₂(Term_app₂(m, n), s) -> Term_app₂(Term_sub₂(m, s), Term_sub₂(n, s))
Term_sub₂(Term_pair₂(m, n), s) -> Term_pair₂(Term_sub₂(m, s), Term_sub₂(n, s))
Term_sub₂(Term_inl₁(m), s) -> Term_inl₁(Term_sub₂(m, s))
Term_sub₂(Term_inr₁(m), s) -> Term_inr₁(Term_sub₂(m, s))
Term_sub₂(Term_var₁(x), Id) -> Term_var₁(x)
Term_sub₂(Term_var₁(x), Cons_usual₃(y, m, s)) -> m
Term_sub₂(Term_var₁(x), Cons_usual₃(y, m, s)) -> Term_sub₂(Term_var₁(x), s)
Term_sub₂(Term_var₁(x), Cons_sum₃(xi, k, s)) -> Term_sub₂(Term_var₁(x), s)
Term_sub₂(Term_sub₂(m, s), t) -> Term_sub₂(m, Concat₂(s, t))
Sum_sub₂(xi, Id) -> Sum_term_var₁(xi)
Sum_sub₂(xi, Cons_sum₃(psi, k, s)) -> Sum_constant₁(k)
Sum_sub₂(xi, Cons_sum₃(psi, k, s)) -> Sum_sub₂(xi, s)
Sum_sub₂(xi, Cons_usual₃(y, m, s)) -> Sum_sub₂(xi, s)
Concat₂(Concat₂(s, t), u) -> Concat₂(s, Concat₂(t, u))
Concat₂(Cons_usual₃(x, m, s), t) -> Cons_usual₃(x, Term_sub₂(m, t), Concat₂(s, t))
Concat₂(Cons_sum₃(xi, k, s), t) -> Cons_sum₃(xi, k, Concat₂(s, t))
Concat₂(Id, s) -> s

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

TERM_SUB₂(Term_var₁(x), Cons_usual₃(y, m, s)) -> TERM_SUB₂(Term_var₁(x), s)
TERM_SUB₂(Term_var₁(x), Cons_sum₃(xi, k, s)) -> TERM_SUB₂(Term_var₁(x), s)

The TRS R consists of the following rules:

Term_sub₂(Case₃(m, xi, n), s) -> Frozen₄(m, Sum_sub₂(xi, s), n, s)
Frozen₄(m, Sum_constant₁(Left), n, s) -> Term_sub₂(m, s)
Frozen₄(m, Sum_constant₁(Right), n, s) -> Term_sub₂(n, s)
Frozen₄(m, Sum_term_var₁(xi), n, s) -> Case₃(Term_sub₂(m, s), xi, Term_sub₂(n, s))
Term_sub₂(Term_app₂(m, n), s) -> Term_app₂(Term_sub₂(m, s), Term_sub₂(n, s))
Term_sub₂(Term_pair₂(m, n), s) -> Term_pair₂(Term_sub₂(m, s), Term_sub₂(n, s))
Term_sub₂(Term_inl₁(m), s) -> Term_inl₁(Term_sub₂(m, s))
Term_sub₂(Term_inr₁(m), s) -> Term_inr₁(Term_sub₂(m, s))
Term_sub₂(Term_var₁(x), Id) -> Term_var₁(x)
Term_sub₂(Term_var₁(x), Cons_usual₃(y, m, s)) -> m
Term_sub₂(Term_var₁(x), Cons_usual₃(y, m, s)) -> Term_sub₂(Term_var₁(x), s)
Term_sub₂(Term_var₁(x), Cons_sum₃(xi, k, s)) -> Term_sub₂(Term_var₁(x), s)
Term_sub₂(Term_sub₂(m, s), t) -> Term_sub₂(m, Concat₂(s, t))
Sum_sub₂(xi, Id) -> Sum_term_var₁(xi)
Sum_sub₂(xi, Cons_sum₃(psi, k, s)) -> Sum_constant₁(k)
Sum_sub₂(xi, Cons_sum₃(psi, k, s)) -> Sum_sub₂(xi, s)
Sum_sub₂(xi, Cons_usual₃(y, m, s)) -> Sum_sub₂(xi, s)
Concat₂(Concat₂(s, t), u) -> Concat₂(s, Concat₂(t, u))
Concat₂(Cons_usual₃(x, m, s), t) -> Cons_usual₃(x, Term_sub₂(m, t), Concat₂(s, t))
Concat₂(Cons_sum₃(xi, k, s), t) -> Cons_sum₃(xi, k, Concat₂(s, t))
Concat₂(Id, s) -> s

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

TERM_SUB₂(Term_var₁(x), Cons_usual₃(y, m, s)) -> TERM_SUB₂(Term_var₁(x), s)

The remaining pairs can at least be oriented weakly.

TERM_SUB₂(Term_var₁(x), Cons_sum₃(xi, k, s)) -> TERM_SUB₂(Term_var₁(x), s)

Used ordering: Polynomial interpretation [21]:

POL(Cons_sum₃(x₁, x₂, x₃)) = 2·x₃
POL(Cons_usual₃(x₁, x₂, x₃)) = 1 + 2·x₃
POL(TERM_SUB₂(x₁, x₂)) = x₁·x₂
POL(Term_var₁(x₁)) = 2

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ QDPOrderProof

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

TERM_SUB₂(Term_var₁(x), Cons_sum₃(xi, k, s)) -> TERM_SUB₂(Term_var₁(x), s)

The TRS R consists of the following rules:

Term_sub₂(Case₃(m, xi, n), s) -> Frozen₄(m, Sum_sub₂(xi, s), n, s)
Frozen₄(m, Sum_constant₁(Left), n, s) -> Term_sub₂(m, s)
Frozen₄(m, Sum_constant₁(Right), n, s) -> Term_sub₂(n, s)
Frozen₄(m, Sum_term_var₁(xi), n, s) -> Case₃(Term_sub₂(m, s), xi, Term_sub₂(n, s))
Term_sub₂(Term_app₂(m, n), s) -> Term_app₂(Term_sub₂(m, s), Term_sub₂(n, s))
Term_sub₂(Term_pair₂(m, n), s) -> Term_pair₂(Term_sub₂(m, s), Term_sub₂(n, s))
Term_sub₂(Term_inl₁(m), s) -> Term_inl₁(Term_sub₂(m, s))
Term_sub₂(Term_inr₁(m), s) -> Term_inr₁(Term_sub₂(m, s))
Term_sub₂(Term_var₁(x), Id) -> Term_var₁(x)
Term_sub₂(Term_var₁(x), Cons_usual₃(y, m, s)) -> m
Term_sub₂(Term_var₁(x), Cons_usual₃(y, m, s)) -> Term_sub₂(Term_var₁(x), s)
Term_sub₂(Term_var₁(x), Cons_sum₃(xi, k, s)) -> Term_sub₂(Term_var₁(x), s)
Term_sub₂(Term_sub₂(m, s), t) -> Term_sub₂(m, Concat₂(s, t))
Sum_sub₂(xi, Id) -> Sum_term_var₁(xi)
Sum_sub₂(xi, Cons_sum₃(psi, k, s)) -> Sum_constant₁(k)
Sum_sub₂(xi, Cons_sum₃(psi, k, s)) -> Sum_sub₂(xi, s)
Sum_sub₂(xi, Cons_usual₃(y, m, s)) -> Sum_sub₂(xi, s)
Concat₂(Concat₂(s, t), u) -> Concat₂(s, Concat₂(t, u))
Concat₂(Cons_usual₃(x, m, s), t) -> Cons_usual₃(x, Term_sub₂(m, t), Concat₂(s, t))
Concat₂(Cons_sum₃(xi, k, s), t) -> Cons_sum₃(xi, k, Concat₂(s, t))
Concat₂(Id, s) -> s

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

TERM_SUB₂(Term_var₁(x), Cons_sum₃(xi, k, s)) -> TERM_SUB₂(Term_var₁(x), s)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [21]:

POL(Cons_sum₃(x₁, x₂, x₃)) = 2 + 2·x₃
POL(TERM_SUB₂(x₁, x₂)) = 2·x₁·x₂
POL(Term_var₁(x₁)) = 2

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

                    ↳ PisEmptyProof

          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

Term_sub₂(Case₃(m, xi, n), s) -> Frozen₄(m, Sum_sub₂(xi, s), n, s)
Frozen₄(m, Sum_constant₁(Left), n, s) -> Term_sub₂(m, s)
Frozen₄(m, Sum_constant₁(Right), n, s) -> Term_sub₂(n, s)
Frozen₄(m, Sum_term_var₁(xi), n, s) -> Case₃(Term_sub₂(m, s), xi, Term_sub₂(n, s))
Term_sub₂(Term_app₂(m, n), s) -> Term_app₂(Term_sub₂(m, s), Term_sub₂(n, s))
Term_sub₂(Term_pair₂(m, n), s) -> Term_pair₂(Term_sub₂(m, s), Term_sub₂(n, s))
Term_sub₂(Term_inl₁(m), s) -> Term_inl₁(Term_sub₂(m, s))
Term_sub₂(Term_inr₁(m), s) -> Term_inr₁(Term_sub₂(m, s))
Term_sub₂(Term_var₁(x), Id) -> Term_var₁(x)
Term_sub₂(Term_var₁(x), Cons_usual₃(y, m, s)) -> m
Term_sub₂(Term_var₁(x), Cons_usual₃(y, m, s)) -> Term_sub₂(Term_var₁(x), s)
Term_sub₂(Term_var₁(x), Cons_sum₃(xi, k, s)) -> Term_sub₂(Term_var₁(x), s)
Term_sub₂(Term_sub₂(m, s), t) -> Term_sub₂(m, Concat₂(s, t))
Sum_sub₂(xi, Id) -> Sum_term_var₁(xi)
Sum_sub₂(xi, Cons_sum₃(psi, k, s)) -> Sum_constant₁(k)
Sum_sub₂(xi, Cons_sum₃(psi, k, s)) -> Sum_sub₂(xi, s)
Sum_sub₂(xi, Cons_usual₃(y, m, s)) -> Sum_sub₂(xi, s)
Concat₂(Concat₂(s, t), u) -> Concat₂(s, Concat₂(t, u))
Concat₂(Cons_usual₃(x, m, s), t) -> Cons_usual₃(x, Term_sub₂(m, t), Concat₂(s, t))
Concat₂(Cons_sum₃(xi, k, s), t) -> Cons_sum₃(xi, k, Concat₂(s, t))
Concat₂(Id, s) -> s

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

TERM_SUB₂(Term_sub₂(m, s), t) -> CONCAT₂(s, t)
TERM_SUB₂(Case₃(m, xi, n), s) -> FROZEN₄(m, Sum_sub₂(xi, s), n, s)
TERM_SUB₂(Term_inl₁(m), s) -> TERM_SUB₂(m, s)
TERM_SUB₂(Term_sub₂(m, s), t) -> TERM_SUB₂(m, Concat₂(s, t))
CONCAT₂(Cons_usual₃(x, m, s), t) -> CONCAT₂(s, t)
CONCAT₂(Concat₂(s, t), u) -> CONCAT₂(s, Concat₂(t, u))
CONCAT₂(Cons_usual₃(x, m, s), t) -> TERM_SUB₂(m, t)
TERM_SUB₂(Term_app₂(m, n), s) -> TERM_SUB₂(n, s)
FROZEN₄(m, Sum_constant₁(Right), n, s) -> TERM_SUB₂(n, s)
CONCAT₂(Concat₂(s, t), u) -> CONCAT₂(t, u)
TERM_SUB₂(Term_pair₂(m, n), s) -> TERM_SUB₂(n, s)
TERM_SUB₂(Term_inr₁(m), s) -> TERM_SUB₂(m, s)
FROZEN₄(m, Sum_constant₁(Left), n, s) -> TERM_SUB₂(m, s)
TERM_SUB₂(Term_app₂(m, n), s) -> TERM_SUB₂(m, s)
FROZEN₄(m, Sum_term_var₁(xi), n, s) -> TERM_SUB₂(n, s)
FROZEN₄(m, Sum_term_var₁(xi), n, s) -> TERM_SUB₂(m, s)
CONCAT₂(Cons_sum₃(xi, k, s), t) -> CONCAT₂(s, t)
TERM_SUB₂(Term_pair₂(m, n), s) -> TERM_SUB₂(m, s)

The TRS R consists of the following rules:

Term_sub₂(Case₃(m, xi, n), s) -> Frozen₄(m, Sum_sub₂(xi, s), n, s)
Frozen₄(m, Sum_constant₁(Left), n, s) -> Term_sub₂(m, s)
Frozen₄(m, Sum_constant₁(Right), n, s) -> Term_sub₂(n, s)
Frozen₄(m, Sum_term_var₁(xi), n, s) -> Case₃(Term_sub₂(m, s), xi, Term_sub₂(n, s))
Term_sub₂(Term_app₂(m, n), s) -> Term_app₂(Term_sub₂(m, s), Term_sub₂(n, s))
Term_sub₂(Term_pair₂(m, n), s) -> Term_pair₂(Term_sub₂(m, s), Term_sub₂(n, s))
Term_sub₂(Term_inl₁(m), s) -> Term_inl₁(Term_sub₂(m, s))
Term_sub₂(Term_inr₁(m), s) -> Term_inr₁(Term_sub₂(m, s))
Term_sub₂(Term_var₁(x), Id) -> Term_var₁(x)
Term_sub₂(Term_var₁(x), Cons_usual₃(y, m, s)) -> m
Term_sub₂(Term_var₁(x), Cons_usual₃(y, m, s)) -> Term_sub₂(Term_var₁(x), s)
Term_sub₂(Term_var₁(x), Cons_sum₃(xi, k, s)) -> Term_sub₂(Term_var₁(x), s)
Term_sub₂(Term_sub₂(m, s), t) -> Term_sub₂(m, Concat₂(s, t))
Sum_sub₂(xi, Id) -> Sum_term_var₁(xi)
Sum_sub₂(xi, Cons_sum₃(psi, k, s)) -> Sum_constant₁(k)
Sum_sub₂(xi, Cons_sum₃(psi, k, s)) -> Sum_sub₂(xi, s)
Sum_sub₂(xi, Cons_usual₃(y, m, s)) -> Sum_sub₂(xi, s)
Concat₂(Concat₂(s, t), u) -> Concat₂(s, Concat₂(t, u))
Concat₂(Cons_usual₃(x, m, s), t) -> Cons_usual₃(x, Term_sub₂(m, t), Concat₂(s, t))
Concat₂(Cons_sum₃(xi, k, s), t) -> Cons_sum₃(xi, k, Concat₂(s, t))
Concat₂(Id, s) -> s

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

TERM_SUB₂(Term_inl₁(m), s) -> TERM_SUB₂(m, s)

The remaining pairs can at least be oriented weakly.

TERM_SUB₂(Term_sub₂(m, s), t) -> CONCAT₂(s, t)
TERM_SUB₂(Case₃(m, xi, n), s) -> FROZEN₄(m, Sum_sub₂(xi, s), n, s)
TERM_SUB₂(Term_sub₂(m, s), t) -> TERM_SUB₂(m, Concat₂(s, t))
CONCAT₂(Cons_usual₃(x, m, s), t) -> CONCAT₂(s, t)
CONCAT₂(Concat₂(s, t), u) -> CONCAT₂(s, Concat₂(t, u))
CONCAT₂(Cons_usual₃(x, m, s), t) -> TERM_SUB₂(m, t)
TERM_SUB₂(Term_app₂(m, n), s) -> TERM_SUB₂(n, s)
FROZEN₄(m, Sum_constant₁(Right), n, s) -> TERM_SUB₂(n, s)
CONCAT₂(Concat₂(s, t), u) -> CONCAT₂(t, u)
TERM_SUB₂(Term_pair₂(m, n), s) -> TERM_SUB₂(n, s)
TERM_SUB₂(Term_inr₁(m), s) -> TERM_SUB₂(m, s)
FROZEN₄(m, Sum_constant₁(Left), n, s) -> TERM_SUB₂(m, s)
TERM_SUB₂(Term_app₂(m, n), s) -> TERM_SUB₂(m, s)
FROZEN₄(m, Sum_term_var₁(xi), n, s) -> TERM_SUB₂(n, s)
FROZEN₄(m, Sum_term_var₁(xi), n, s) -> TERM_SUB₂(m, s)
CONCAT₂(Cons_sum₃(xi, k, s), t) -> CONCAT₂(s, t)
TERM_SUB₂(Term_pair₂(m, n), s) -> TERM_SUB₂(m, s)

Used ordering: Polynomial interpretation [21]:

POL(CONCAT₂(x₁, x₂)) = 2·x₁
POL(Case₃(x₁, x₂, x₃)) = 2·x₁ + 2·x₃
POL(Concat₂(x₁, x₂)) = 2·x₁ + 2·x₂
POL(Cons_sum₃(x₁, x₂, x₃)) = 2·x₃
POL(Cons_usual₃(x₁, x₂, x₃)) = 2·x₂ + 2·x₃
POL(FROZEN₄(x₁, x₂, x₃, x₄)) = 2·x₁ + 2·x₃
POL(Frozen₄(x₁, x₂, x₃, x₄)) = 0
POL(Id) = 0
POL(Left) = 0
POL(Right) = 0
POL(Sum_constant₁(x₁)) = 0
POL(Sum_sub₂(x₁, x₂)) = 0
POL(Sum_term_var₁(x₁)) = 0
POL(TERM_SUB₂(x₁, x₂)) = x₁
POL(Term_app₂(x₁, x₂)) = 2·x₁ + 2·x₂
POL(Term_inl₁(x₁)) = 1 + 2·x₁
POL(Term_inr₁(x₁)) = 2·x₁
POL(Term_pair₂(x₁, x₂)) = 2·x₁ + 2·x₂
POL(Term_sub₂(x₁, x₂)) = 2·x₁ + 2·x₂
POL(Term_var₁(x₁)) = 0

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

TERM_SUB₂(Term_sub₂(m, s), t) -> CONCAT₂(s, t)
TERM_SUB₂(Case₃(m, xi, n), s) -> FROZEN₄(m, Sum_sub₂(xi, s), n, s)
TERM_SUB₂(Term_sub₂(m, s), t) -> TERM_SUB₂(m, Concat₂(s, t))
CONCAT₂(Cons_usual₃(x, m, s), t) -> CONCAT₂(s, t)
CONCAT₂(Concat₂(s, t), u) -> CONCAT₂(s, Concat₂(t, u))
CONCAT₂(Cons_usual₃(x, m, s), t) -> TERM_SUB₂(m, t)
TERM_SUB₂(Term_app₂(m, n), s) -> TERM_SUB₂(n, s)
FROZEN₄(m, Sum_constant₁(Right), n, s) -> TERM_SUB₂(n, s)
CONCAT₂(Concat₂(s, t), u) -> CONCAT₂(t, u)
TERM_SUB₂(Term_pair₂(m, n), s) -> TERM_SUB₂(n, s)
TERM_SUB₂(Term_inr₁(m), s) -> TERM_SUB₂(m, s)
FROZEN₄(m, Sum_constant₁(Left), n, s) -> TERM_SUB₂(m, s)
TERM_SUB₂(Term_app₂(m, n), s) -> TERM_SUB₂(m, s)
FROZEN₄(m, Sum_term_var₁(xi), n, s) -> TERM_SUB₂(n, s)
FROZEN₄(m, Sum_term_var₁(xi), n, s) -> TERM_SUB₂(m, s)
CONCAT₂(Cons_sum₃(xi, k, s), t) -> CONCAT₂(s, t)
TERM_SUB₂(Term_pair₂(m, n), s) -> TERM_SUB₂(m, s)

The TRS R consists of the following rules:

Term_sub₂(Case₃(m, xi, n), s) -> Frozen₄(m, Sum_sub₂(xi, s), n, s)
Frozen₄(m, Sum_constant₁(Left), n, s) -> Term_sub₂(m, s)
Frozen₄(m, Sum_constant₁(Right), n, s) -> Term_sub₂(n, s)
Frozen₄(m, Sum_term_var₁(xi), n, s) -> Case₃(Term_sub₂(m, s), xi, Term_sub₂(n, s))
Term_sub₂(Term_app₂(m, n), s) -> Term_app₂(Term_sub₂(m, s), Term_sub₂(n, s))
Term_sub₂(Term_pair₂(m, n), s) -> Term_pair₂(Term_sub₂(m, s), Term_sub₂(n, s))
Term_sub₂(Term_inl₁(m), s) -> Term_inl₁(Term_sub₂(m, s))
Term_sub₂(Term_inr₁(m), s) -> Term_inr₁(Term_sub₂(m, s))
Term_sub₂(Term_var₁(x), Id) -> Term_var₁(x)
Term_sub₂(Term_var₁(x), Cons_usual₃(y, m, s)) -> m
Term_sub₂(Term_var₁(x), Cons_usual₃(y, m, s)) -> Term_sub₂(Term_var₁(x), s)
Term_sub₂(Term_var₁(x), Cons_sum₃(xi, k, s)) -> Term_sub₂(Term_var₁(x), s)
Term_sub₂(Term_sub₂(m, s), t) -> Term_sub₂(m, Concat₂(s, t))
Sum_sub₂(xi, Id) -> Sum_term_var₁(xi)
Sum_sub₂(xi, Cons_sum₃(psi, k, s)) -> Sum_constant₁(k)
Sum_sub₂(xi, Cons_sum₃(psi, k, s)) -> Sum_sub₂(xi, s)
Sum_sub₂(xi, Cons_usual₃(y, m, s)) -> Sum_sub₂(xi, s)
Concat₂(Concat₂(s, t), u) -> Concat₂(s, Concat₂(t, u))
Concat₂(Cons_usual₃(x, m, s), t) -> Cons_usual₃(x, Term_sub₂(m, t), Concat₂(s, t))
Concat₂(Cons_sum₃(xi, k, s), t) -> Cons_sum₃(xi, k, Concat₂(s, t))
Concat₂(Id, s) -> s

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

CONCAT₂(Cons_sum₃(xi, k, s), t) -> CONCAT₂(s, t)

The remaining pairs can at least be oriented weakly.

TERM_SUB₂(Term_sub₂(m, s), t) -> CONCAT₂(s, t)
TERM_SUB₂(Case₃(m, xi, n), s) -> FROZEN₄(m, Sum_sub₂(xi, s), n, s)
TERM_SUB₂(Term_sub₂(m, s), t) -> TERM_SUB₂(m, Concat₂(s, t))
CONCAT₂(Cons_usual₃(x, m, s), t) -> CONCAT₂(s, t)
CONCAT₂(Concat₂(s, t), u) -> CONCAT₂(s, Concat₂(t, u))
CONCAT₂(Cons_usual₃(x, m, s), t) -> TERM_SUB₂(m, t)
TERM_SUB₂(Term_app₂(m, n), s) -> TERM_SUB₂(n, s)
FROZEN₄(m, Sum_constant₁(Right), n, s) -> TERM_SUB₂(n, s)
CONCAT₂(Concat₂(s, t), u) -> CONCAT₂(t, u)
TERM_SUB₂(Term_pair₂(m, n), s) -> TERM_SUB₂(n, s)
TERM_SUB₂(Term_inr₁(m), s) -> TERM_SUB₂(m, s)
FROZEN₄(m, Sum_constant₁(Left), n, s) -> TERM_SUB₂(m, s)
TERM_SUB₂(Term_app₂(m, n), s) -> TERM_SUB₂(m, s)
FROZEN₄(m, Sum_term_var₁(xi), n, s) -> TERM_SUB₂(n, s)
FROZEN₄(m, Sum_term_var₁(xi), n, s) -> TERM_SUB₂(m, s)
TERM_SUB₂(Term_pair₂(m, n), s) -> TERM_SUB₂(m, s)

Used ordering: Polynomial interpretation [21]:

POL(CONCAT₂(x₁, x₂)) = x₁
POL(Case₃(x₁, x₂, x₃)) = 2·x₁ + 2·x₃
POL(Concat₂(x₁, x₂)) = 2·x₁ + 2·x₂
POL(Cons_sum₃(x₁, x₂, x₃)) = 1 + 2·x₃
POL(Cons_usual₃(x₁, x₂, x₃)) = 2·x₂ + 2·x₃
POL(FROZEN₄(x₁, x₂, x₃, x₄)) = 2·x₁ + 2·x₃
POL(Frozen₄(x₁, x₂, x₃, x₄)) = 0
POL(Id) = 0
POL(Left) = 0
POL(Right) = 0
POL(Sum_constant₁(x₁)) = 0
POL(Sum_sub₂(x₁, x₂)) = 0
POL(Sum_term_var₁(x₁)) = 0
POL(TERM_SUB₂(x₁, x₂)) = 2·x₁
POL(Term_app₂(x₁, x₂)) = 2·x₁ + 2·x₂
POL(Term_inl₁(x₁)) = 0
POL(Term_inr₁(x₁)) = 2·x₁
POL(Term_pair₂(x₁, x₂)) = 2·x₁ + 2·x₂
POL(Term_sub₂(x₁, x₂)) = 2·x₁ + 2·x₂
POL(Term_var₁(x₁)) = 0

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

                    ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

TERM_SUB₂(Term_sub₂(m, s), t) -> CONCAT₂(s, t)
TERM_SUB₂(Case₃(m, xi, n), s) -> FROZEN₄(m, Sum_sub₂(xi, s), n, s)
TERM_SUB₂(Term_sub₂(m, s), t) -> TERM_SUB₂(m, Concat₂(s, t))
CONCAT₂(Cons_usual₃(x, m, s), t) -> CONCAT₂(s, t)
CONCAT₂(Concat₂(s, t), u) -> CONCAT₂(s, Concat₂(t, u))
CONCAT₂(Cons_usual₃(x, m, s), t) -> TERM_SUB₂(m, t)
TERM_SUB₂(Term_app₂(m, n), s) -> TERM_SUB₂(n, s)
FROZEN₄(m, Sum_constant₁(Right), n, s) -> TERM_SUB₂(n, s)
CONCAT₂(Concat₂(s, t), u) -> CONCAT₂(t, u)
TERM_SUB₂(Term_pair₂(m, n), s) -> TERM_SUB₂(n, s)
TERM_SUB₂(Term_inr₁(m), s) -> TERM_SUB₂(m, s)
FROZEN₄(m, Sum_constant₁(Left), n, s) -> TERM_SUB₂(m, s)
TERM_SUB₂(Term_app₂(m, n), s) -> TERM_SUB₂(m, s)
FROZEN₄(m, Sum_term_var₁(xi), n, s) -> TERM_SUB₂(n, s)
FROZEN₄(m, Sum_term_var₁(xi), n, s) -> TERM_SUB₂(m, s)
TERM_SUB₂(Term_pair₂(m, n), s) -> TERM_SUB₂(m, s)

The TRS R consists of the following rules:

Term_sub₂(Case₃(m, xi, n), s) -> Frozen₄(m, Sum_sub₂(xi, s), n, s)
Frozen₄(m, Sum_constant₁(Left), n, s) -> Term_sub₂(m, s)
Frozen₄(m, Sum_constant₁(Right), n, s) -> Term_sub₂(n, s)
Frozen₄(m, Sum_term_var₁(xi), n, s) -> Case₃(Term_sub₂(m, s), xi, Term_sub₂(n, s))
Term_sub₂(Term_app₂(m, n), s) -> Term_app₂(Term_sub₂(m, s), Term_sub₂(n, s))
Term_sub₂(Term_pair₂(m, n), s) -> Term_pair₂(Term_sub₂(m, s), Term_sub₂(n, s))
Term_sub₂(Term_inl₁(m), s) -> Term_inl₁(Term_sub₂(m, s))
Term_sub₂(Term_inr₁(m), s) -> Term_inr₁(Term_sub₂(m, s))
Term_sub₂(Term_var₁(x), Id) -> Term_var₁(x)
Term_sub₂(Term_var₁(x), Cons_usual₃(y, m, s)) -> m
Term_sub₂(Term_var₁(x), Cons_usual₃(y, m, s)) -> Term_sub₂(Term_var₁(x), s)
Term_sub₂(Term_var₁(x), Cons_sum₃(xi, k, s)) -> Term_sub₂(Term_var₁(x), s)
Term_sub₂(Term_sub₂(m, s), t) -> Term_sub₂(m, Concat₂(s, t))
Sum_sub₂(xi, Id) -> Sum_term_var₁(xi)
Sum_sub₂(xi, Cons_sum₃(psi, k, s)) -> Sum_constant₁(k)
Sum_sub₂(xi, Cons_sum₃(psi, k, s)) -> Sum_sub₂(xi, s)
Sum_sub₂(xi, Cons_usual₃(y, m, s)) -> Sum_sub₂(xi, s)
Concat₂(Concat₂(s, t), u) -> Concat₂(s, Concat₂(t, u))
Concat₂(Cons_usual₃(x, m, s), t) -> Cons_usual₃(x, Term_sub₂(m, t), Concat₂(s, t))
Concat₂(Cons_sum₃(xi, k, s), t) -> Cons_sum₃(xi, k, Concat₂(s, t))
Concat₂(Id, s) -> s

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

TERM_SUB₂(Term_inr₁(m), s) -> TERM_SUB₂(m, s)

The remaining pairs can at least be oriented weakly.

TERM_SUB₂(Term_sub₂(m, s), t) -> CONCAT₂(s, t)
TERM_SUB₂(Case₃(m, xi, n), s) -> FROZEN₄(m, Sum_sub₂(xi, s), n, s)
TERM_SUB₂(Term_sub₂(m, s), t) -> TERM_SUB₂(m, Concat₂(s, t))
CONCAT₂(Cons_usual₃(x, m, s), t) -> CONCAT₂(s, t)
CONCAT₂(Concat₂(s, t), u) -> CONCAT₂(s, Concat₂(t, u))
CONCAT₂(Cons_usual₃(x, m, s), t) -> TERM_SUB₂(m, t)
TERM_SUB₂(Term_app₂(m, n), s) -> TERM_SUB₂(n, s)
FROZEN₄(m, Sum_constant₁(Right), n, s) -> TERM_SUB₂(n, s)
CONCAT₂(Concat₂(s, t), u) -> CONCAT₂(t, u)
TERM_SUB₂(Term_pair₂(m, n), s) -> TERM_SUB₂(n, s)
FROZEN₄(m, Sum_constant₁(Left), n, s) -> TERM_SUB₂(m, s)
TERM_SUB₂(Term_app₂(m, n), s) -> TERM_SUB₂(m, s)
FROZEN₄(m, Sum_term_var₁(xi), n, s) -> TERM_SUB₂(n, s)
FROZEN₄(m, Sum_term_var₁(xi), n, s) -> TERM_SUB₂(m, s)
TERM_SUB₂(Term_pair₂(m, n), s) -> TERM_SUB₂(m, s)

Used ordering: Polynomial interpretation [21]:

POL(CONCAT₂(x₁, x₂)) = 2·x₁
POL(Case₃(x₁, x₂, x₃)) = 2·x₁ + 2·x₃
POL(Concat₂(x₁, x₂)) = 2·x₁ + 2·x₂
POL(Cons_sum₃(x₁, x₂, x₃)) = 0
POL(Cons_usual₃(x₁, x₂, x₃)) = 2·x₂ + 2·x₃
POL(FROZEN₄(x₁, x₂, x₃, x₄)) = 2·x₁ + 2·x₃
POL(Frozen₄(x₁, x₂, x₃, x₄)) = 0
POL(Id) = 0
POL(Left) = 0
POL(Right) = 0
POL(Sum_constant₁(x₁)) = 0
POL(Sum_sub₂(x₁, x₂)) = 0
POL(Sum_term_var₁(x₁)) = 0
POL(TERM_SUB₂(x₁, x₂)) = x₁
POL(Term_app₂(x₁, x₂)) = 2·x₁ + 2·x₂
POL(Term_inl₁(x₁)) = 0
POL(Term_inr₁(x₁)) = 1 + 2·x₁
POL(Term_pair₂(x₁, x₂)) = 2·x₁ + 2·x₂
POL(Term_sub₂(x₁, x₂)) = 2·x₁ + 2·x₂
POL(Term_var₁(x₁)) = 0

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

                    ↳ QDPOrderProof

                      ↳ QDP

                        ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

TERM_SUB₂(Term_sub₂(m, s), t) -> CONCAT₂(s, t)
TERM_SUB₂(Case₃(m, xi, n), s) -> FROZEN₄(m, Sum_sub₂(xi, s), n, s)
TERM_SUB₂(Term_sub₂(m, s), t) -> TERM_SUB₂(m, Concat₂(s, t))
CONCAT₂(Cons_usual₃(x, m, s), t) -> CONCAT₂(s, t)
CONCAT₂(Concat₂(s, t), u) -> CONCAT₂(s, Concat₂(t, u))
CONCAT₂(Cons_usual₃(x, m, s), t) -> TERM_SUB₂(m, t)
TERM_SUB₂(Term_app₂(m, n), s) -> TERM_SUB₂(n, s)
FROZEN₄(m, Sum_constant₁(Right), n, s) -> TERM_SUB₂(n, s)
CONCAT₂(Concat₂(s, t), u) -> CONCAT₂(t, u)
TERM_SUB₂(Term_pair₂(m, n), s) -> TERM_SUB₂(n, s)
FROZEN₄(m, Sum_constant₁(Left), n, s) -> TERM_SUB₂(m, s)
TERM_SUB₂(Term_app₂(m, n), s) -> TERM_SUB₂(m, s)
FROZEN₄(m, Sum_term_var₁(xi), n, s) -> TERM_SUB₂(n, s)
FROZEN₄(m, Sum_term_var₁(xi), n, s) -> TERM_SUB₂(m, s)
TERM_SUB₂(Term_pair₂(m, n), s) -> TERM_SUB₂(m, s)

The TRS R consists of the following rules:

Term_sub₂(Case₃(m, xi, n), s) -> Frozen₄(m, Sum_sub₂(xi, s), n, s)
Frozen₄(m, Sum_constant₁(Left), n, s) -> Term_sub₂(m, s)
Frozen₄(m, Sum_constant₁(Right), n, s) -> Term_sub₂(n, s)
Frozen₄(m, Sum_term_var₁(xi), n, s) -> Case₃(Term_sub₂(m, s), xi, Term_sub₂(n, s))
Term_sub₂(Term_app₂(m, n), s) -> Term_app₂(Term_sub₂(m, s), Term_sub₂(n, s))
Term_sub₂(Term_pair₂(m, n), s) -> Term_pair₂(Term_sub₂(m, s), Term_sub₂(n, s))
Term_sub₂(Term_inl₁(m), s) -> Term_inl₁(Term_sub₂(m, s))
Term_sub₂(Term_inr₁(m), s) -> Term_inr₁(Term_sub₂(m, s))
Term_sub₂(Term_var₁(x), Id) -> Term_var₁(x)
Term_sub₂(Term_var₁(x), Cons_usual₃(y, m, s)) -> m
Term_sub₂(Term_var₁(x), Cons_usual₃(y, m, s)) -> Term_sub₂(Term_var₁(x), s)
Term_sub₂(Term_var₁(x), Cons_sum₃(xi, k, s)) -> Term_sub₂(Term_var₁(x), s)
Term_sub₂(Term_sub₂(m, s), t) -> Term_sub₂(m, Concat₂(s, t))
Sum_sub₂(xi, Id) -> Sum_term_var₁(xi)
Sum_sub₂(xi, Cons_sum₃(psi, k, s)) -> Sum_constant₁(k)
Sum_sub₂(xi, Cons_sum₃(psi, k, s)) -> Sum_sub₂(xi, s)
Sum_sub₂(xi, Cons_usual₃(y, m, s)) -> Sum_sub₂(xi, s)
Concat₂(Concat₂(s, t), u) -> Concat₂(s, Concat₂(t, u))
Concat₂(Cons_usual₃(x, m, s), t) -> Cons_usual₃(x, Term_sub₂(m, t), Concat₂(s, t))
Concat₂(Cons_sum₃(xi, k, s), t) -> Cons_sum₃(xi, k, Concat₂(s, t))
Concat₂(Id, s) -> s

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

TERM_SUB₂(Term_sub₂(m, s), t) -> CONCAT₂(s, t)
TERM_SUB₂(Term_sub₂(m, s), t) -> TERM_SUB₂(m, Concat₂(s, t))

The remaining pairs can at least be oriented weakly.

TERM_SUB₂(Case₃(m, xi, n), s) -> FROZEN₄(m, Sum_sub₂(xi, s), n, s)
CONCAT₂(Cons_usual₃(x, m, s), t) -> CONCAT₂(s, t)
CONCAT₂(Concat₂(s, t), u) -> CONCAT₂(s, Concat₂(t, u))
CONCAT₂(Cons_usual₃(x, m, s), t) -> TERM_SUB₂(m, t)
TERM_SUB₂(Term_app₂(m, n), s) -> TERM_SUB₂(n, s)
FROZEN₄(m, Sum_constant₁(Right), n, s) -> TERM_SUB₂(n, s)
CONCAT₂(Concat₂(s, t), u) -> CONCAT₂(t, u)
TERM_SUB₂(Term_pair₂(m, n), s) -> TERM_SUB₂(n, s)
FROZEN₄(m, Sum_constant₁(Left), n, s) -> TERM_SUB₂(m, s)
TERM_SUB₂(Term_app₂(m, n), s) -> TERM_SUB₂(m, s)
FROZEN₄(m, Sum_term_var₁(xi), n, s) -> TERM_SUB₂(n, s)
FROZEN₄(m, Sum_term_var₁(xi), n, s) -> TERM_SUB₂(m, s)
TERM_SUB₂(Term_pair₂(m, n), s) -> TERM_SUB₂(m, s)

Used ordering: Polynomial interpretation [21]:

POL(CONCAT₂(x₁, x₂)) = 2·x₁
POL(Case₃(x₁, x₂, x₃)) = 2·x₁ + 2·x₃
POL(Concat₂(x₁, x₂)) = 2·x₁ + 2·x₂
POL(Cons_sum₃(x₁, x₂, x₃)) = 0
POL(Cons_usual₃(x₁, x₂, x₃)) = 2·x₂ + 2·x₃
POL(FROZEN₄(x₁, x₂, x₃, x₄)) = 2·x₁ + 2·x₃
POL(Frozen₄(x₁, x₂, x₃, x₄)) = 0
POL(Id) = 0
POL(Left) = 0
POL(Right) = 0
POL(Sum_constant₁(x₁)) = 0
POL(Sum_sub₂(x₁, x₂)) = 0
POL(Sum_term_var₁(x₁)) = 0
POL(TERM_SUB₂(x₁, x₂)) = x₁
POL(Term_app₂(x₁, x₂)) = 2·x₁ + 2·x₂
POL(Term_inl₁(x₁)) = 0
POL(Term_inr₁(x₁)) = 0
POL(Term_pair₂(x₁, x₂)) = 2·x₁ + 2·x₂
POL(Term_sub₂(x₁, x₂)) = 1 + 2·x₁ + 2·x₂
POL(Term_var₁(x₁)) = 0

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

                    ↳ QDPOrderProof

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

TERM_SUB₂(Case₃(m, xi, n), s) -> FROZEN₄(m, Sum_sub₂(xi, s), n, s)
CONCAT₂(Cons_usual₃(x, m, s), t) -> CONCAT₂(s, t)
CONCAT₂(Concat₂(s, t), u) -> CONCAT₂(s, Concat₂(t, u))
CONCAT₂(Cons_usual₃(x, m, s), t) -> TERM_SUB₂(m, t)
TERM_SUB₂(Term_app₂(m, n), s) -> TERM_SUB₂(n, s)
FROZEN₄(m, Sum_constant₁(Right), n, s) -> TERM_SUB₂(n, s)
CONCAT₂(Concat₂(s, t), u) -> CONCAT₂(t, u)
TERM_SUB₂(Term_pair₂(m, n), s) -> TERM_SUB₂(n, s)
FROZEN₄(m, Sum_constant₁(Left), n, s) -> TERM_SUB₂(m, s)
TERM_SUB₂(Term_app₂(m, n), s) -> TERM_SUB₂(m, s)
FROZEN₄(m, Sum_term_var₁(xi), n, s) -> TERM_SUB₂(n, s)
FROZEN₄(m, Sum_term_var₁(xi), n, s) -> TERM_SUB₂(m, s)
TERM_SUB₂(Term_pair₂(m, n), s) -> TERM_SUB₂(m, s)

The TRS R consists of the following rules:

Term_sub₂(Case₃(m, xi, n), s) -> Frozen₄(m, Sum_sub₂(xi, s), n, s)
Frozen₄(m, Sum_constant₁(Left), n, s) -> Term_sub₂(m, s)
Frozen₄(m, Sum_constant₁(Right), n, s) -> Term_sub₂(n, s)
Frozen₄(m, Sum_term_var₁(xi), n, s) -> Case₃(Term_sub₂(m, s), xi, Term_sub₂(n, s))
Term_sub₂(Term_app₂(m, n), s) -> Term_app₂(Term_sub₂(m, s), Term_sub₂(n, s))
Term_sub₂(Term_pair₂(m, n), s) -> Term_pair₂(Term_sub₂(m, s), Term_sub₂(n, s))
Term_sub₂(Term_inl₁(m), s) -> Term_inl₁(Term_sub₂(m, s))
Term_sub₂(Term_inr₁(m), s) -> Term_inr₁(Term_sub₂(m, s))
Term_sub₂(Term_var₁(x), Id) -> Term_var₁(x)
Term_sub₂(Term_var₁(x), Cons_usual₃(y, m, s)) -> m
Term_sub₂(Term_var₁(x), Cons_usual₃(y, m, s)) -> Term_sub₂(Term_var₁(x), s)
Term_sub₂(Term_var₁(x), Cons_sum₃(xi, k, s)) -> Term_sub₂(Term_var₁(x), s)
Term_sub₂(Term_sub₂(m, s), t) -> Term_sub₂(m, Concat₂(s, t))
Sum_sub₂(xi, Id) -> Sum_term_var₁(xi)
Sum_sub₂(xi, Cons_sum₃(psi, k, s)) -> Sum_constant₁(k)
Sum_sub₂(xi, Cons_sum₃(psi, k, s)) -> Sum_sub₂(xi, s)
Sum_sub₂(xi, Cons_usual₃(y, m, s)) -> Sum_sub₂(xi, s)
Concat₂(Concat₂(s, t), u) -> Concat₂(s, Concat₂(t, u))
Concat₂(Cons_usual₃(x, m, s), t) -> Cons_usual₃(x, Term_sub₂(m, t), Concat₂(s, t))
Concat₂(Cons_sum₃(xi, k, s), t) -> Cons_sum₃(xi, k, Concat₂(s, t))
Concat₂(Id, s) -> s

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 2 SCCs with 1 less node.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

                    ↳ QDPOrderProof

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ AND

                                ↳ QDP

                                  ↳ QDPOrderProof

                                ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

TERM_SUB₂(Case₃(m, xi, n), s) -> FROZEN₄(m, Sum_sub₂(xi, s), n, s)
TERM_SUB₂(Term_pair₂(m, n), s) -> TERM_SUB₂(n, s)
FROZEN₄(m, Sum_constant₁(Left), n, s) -> TERM_SUB₂(m, s)
TERM_SUB₂(Term_app₂(m, n), s) -> TERM_SUB₂(m, s)
FROZEN₄(m, Sum_term_var₁(xi), n, s) -> TERM_SUB₂(n, s)
TERM_SUB₂(Term_app₂(m, n), s) -> TERM_SUB₂(n, s)
FROZEN₄(m, Sum_term_var₁(xi), n, s) -> TERM_SUB₂(m, s)
FROZEN₄(m, Sum_constant₁(Right), n, s) -> TERM_SUB₂(n, s)
TERM_SUB₂(Term_pair₂(m, n), s) -> TERM_SUB₂(m, s)

The TRS R consists of the following rules:

Term_sub₂(Case₃(m, xi, n), s) -> Frozen₄(m, Sum_sub₂(xi, s), n, s)
Frozen₄(m, Sum_constant₁(Left), n, s) -> Term_sub₂(m, s)
Frozen₄(m, Sum_constant₁(Right), n, s) -> Term_sub₂(n, s)
Frozen₄(m, Sum_term_var₁(xi), n, s) -> Case₃(Term_sub₂(m, s), xi, Term_sub₂(n, s))
Term_sub₂(Term_app₂(m, n), s) -> Term_app₂(Term_sub₂(m, s), Term_sub₂(n, s))
Term_sub₂(Term_pair₂(m, n), s) -> Term_pair₂(Term_sub₂(m, s), Term_sub₂(n, s))
Term_sub₂(Term_inl₁(m), s) -> Term_inl₁(Term_sub₂(m, s))
Term_sub₂(Term_inr₁(m), s) -> Term_inr₁(Term_sub₂(m, s))
Term_sub₂(Term_var₁(x), Id) -> Term_var₁(x)
Term_sub₂(Term_var₁(x), Cons_usual₃(y, m, s)) -> m
Term_sub₂(Term_var₁(x), Cons_usual₃(y, m, s)) -> Term_sub₂(Term_var₁(x), s)
Term_sub₂(Term_var₁(x), Cons_sum₃(xi, k, s)) -> Term_sub₂(Term_var₁(x), s)
Term_sub₂(Term_sub₂(m, s), t) -> Term_sub₂(m, Concat₂(s, t))
Sum_sub₂(xi, Id) -> Sum_term_var₁(xi)
Sum_sub₂(xi, Cons_sum₃(psi, k, s)) -> Sum_constant₁(k)
Sum_sub₂(xi, Cons_sum₃(psi, k, s)) -> Sum_sub₂(xi, s)
Sum_sub₂(xi, Cons_usual₃(y, m, s)) -> Sum_sub₂(xi, s)
Concat₂(Concat₂(s, t), u) -> Concat₂(s, Concat₂(t, u))
Concat₂(Cons_usual₃(x, m, s), t) -> Cons_usual₃(x, Term_sub₂(m, t), Concat₂(s, t))
Concat₂(Cons_sum₃(xi, k, s), t) -> Cons_sum₃(xi, k, Concat₂(s, t))
Concat₂(Id, s) -> s

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

TERM_SUB₂(Term_app₂(m, n), s) -> TERM_SUB₂(m, s)
TERM_SUB₂(Term_app₂(m, n), s) -> TERM_SUB₂(n, s)

The remaining pairs can at least be oriented weakly.

TERM_SUB₂(Case₃(m, xi, n), s) -> FROZEN₄(m, Sum_sub₂(xi, s), n, s)
TERM_SUB₂(Term_pair₂(m, n), s) -> TERM_SUB₂(n, s)
FROZEN₄(m, Sum_constant₁(Left), n, s) -> TERM_SUB₂(m, s)
FROZEN₄(m, Sum_term_var₁(xi), n, s) -> TERM_SUB₂(n, s)
FROZEN₄(m, Sum_term_var₁(xi), n, s) -> TERM_SUB₂(m, s)
FROZEN₄(m, Sum_constant₁(Right), n, s) -> TERM_SUB₂(n, s)
TERM_SUB₂(Term_pair₂(m, n), s) -> TERM_SUB₂(m, s)

Used ordering: Polynomial interpretation [21]:

POL(Case₃(x₁, x₂, x₃)) = 2·x₁ + 2·x₃
POL(Cons_sum₃(x₁, x₂, x₃)) = 0
POL(Cons_usual₃(x₁, x₂, x₃)) = 0
POL(FROZEN₄(x₁, x₂, x₃, x₄)) = 2·x₁ + 2·x₃
POL(Id) = 0
POL(Left) = 0
POL(Right) = 0
POL(Sum_constant₁(x₁)) = 0
POL(Sum_sub₂(x₁, x₂)) = 0
POL(Sum_term_var₁(x₁)) = 0
POL(TERM_SUB₂(x₁, x₂)) = 2·x₁
POL(Term_app₂(x₁, x₂)) = 2 + 2·x₁ + 2·x₂
POL(Term_pair₂(x₁, x₂)) = 2·x₁ + 2·x₂

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

                    ↳ QDPOrderProof

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ AND

                                ↳ QDP

                                  ↳ QDPOrderProof

                                    ↳ QDP

                                      ↳ QDPOrderProof

                                ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

TERM_SUB₂(Case₃(m, xi, n), s) -> FROZEN₄(m, Sum_sub₂(xi, s), n, s)
TERM_SUB₂(Term_pair₂(m, n), s) -> TERM_SUB₂(n, s)
FROZEN₄(m, Sum_constant₁(Left), n, s) -> TERM_SUB₂(m, s)
FROZEN₄(m, Sum_term_var₁(xi), n, s) -> TERM_SUB₂(n, s)
FROZEN₄(m, Sum_term_var₁(xi), n, s) -> TERM_SUB₂(m, s)
FROZEN₄(m, Sum_constant₁(Right), n, s) -> TERM_SUB₂(n, s)
TERM_SUB₂(Term_pair₂(m, n), s) -> TERM_SUB₂(m, s)

The TRS R consists of the following rules:

Term_sub₂(Case₃(m, xi, n), s) -> Frozen₄(m, Sum_sub₂(xi, s), n, s)
Frozen₄(m, Sum_constant₁(Left), n, s) -> Term_sub₂(m, s)
Frozen₄(m, Sum_constant₁(Right), n, s) -> Term_sub₂(n, s)
Frozen₄(m, Sum_term_var₁(xi), n, s) -> Case₃(Term_sub₂(m, s), xi, Term_sub₂(n, s))
Term_sub₂(Term_app₂(m, n), s) -> Term_app₂(Term_sub₂(m, s), Term_sub₂(n, s))
Term_sub₂(Term_pair₂(m, n), s) -> Term_pair₂(Term_sub₂(m, s), Term_sub₂(n, s))
Term_sub₂(Term_inl₁(m), s) -> Term_inl₁(Term_sub₂(m, s))
Term_sub₂(Term_inr₁(m), s) -> Term_inr₁(Term_sub₂(m, s))
Term_sub₂(Term_var₁(x), Id) -> Term_var₁(x)
Term_sub₂(Term_var₁(x), Cons_usual₃(y, m, s)) -> m
Term_sub₂(Term_var₁(x), Cons_usual₃(y, m, s)) -> Term_sub₂(Term_var₁(x), s)
Term_sub₂(Term_var₁(x), Cons_sum₃(xi, k, s)) -> Term_sub₂(Term_var₁(x), s)
Term_sub₂(Term_sub₂(m, s), t) -> Term_sub₂(m, Concat₂(s, t))
Sum_sub₂(xi, Id) -> Sum_term_var₁(xi)
Sum_sub₂(xi, Cons_sum₃(psi, k, s)) -> Sum_constant₁(k)
Sum_sub₂(xi, Cons_sum₃(psi, k, s)) -> Sum_sub₂(xi, s)
Sum_sub₂(xi, Cons_usual₃(y, m, s)) -> Sum_sub₂(xi, s)
Concat₂(Concat₂(s, t), u) -> Concat₂(s, Concat₂(t, u))
Concat₂(Cons_usual₃(x, m, s), t) -> Cons_usual₃(x, Term_sub₂(m, t), Concat₂(s, t))
Concat₂(Cons_sum₃(xi, k, s), t) -> Cons_sum₃(xi, k, Concat₂(s, t))
Concat₂(Id, s) -> s

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

TERM_SUB₂(Term_pair₂(m, n), s) -> TERM_SUB₂(n, s)
TERM_SUB₂(Term_pair₂(m, n), s) -> TERM_SUB₂(m, s)

The remaining pairs can at least be oriented weakly.

TERM_SUB₂(Case₃(m, xi, n), s) -> FROZEN₄(m, Sum_sub₂(xi, s), n, s)
FROZEN₄(m, Sum_constant₁(Left), n, s) -> TERM_SUB₂(m, s)
FROZEN₄(m, Sum_term_var₁(xi), n, s) -> TERM_SUB₂(n, s)
FROZEN₄(m, Sum_term_var₁(xi), n, s) -> TERM_SUB₂(m, s)
FROZEN₄(m, Sum_constant₁(Right), n, s) -> TERM_SUB₂(n, s)

Used ordering: Polynomial interpretation [21]:

POL(Case₃(x₁, x₂, x₃)) = 2·x₁ + 2·x₃
POL(Cons_sum₃(x₁, x₂, x₃)) = 0
POL(Cons_usual₃(x₁, x₂, x₃)) = 0
POL(FROZEN₄(x₁, x₂, x₃, x₄)) = 2·x₁ + 2·x₃
POL(Id) = 0
POL(Left) = 0
POL(Right) = 0
POL(Sum_constant₁(x₁)) = 0
POL(Sum_sub₂(x₁, x₂)) = 0
POL(Sum_term_var₁(x₁)) = 0
POL(TERM_SUB₂(x₁, x₂)) = 2·x₁
POL(Term_pair₂(x₁, x₂)) = 2 + 2·x₁ + 2·x₂

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

                    ↳ QDPOrderProof

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ AND

                                ↳ QDP

                                  ↳ QDPOrderProof

                                    ↳ QDP

                                      ↳ QDPOrderProof

                                        ↳ QDP

                                          ↳ QDPOrderProof

                                ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

TERM_SUB₂(Case₃(m, xi, n), s) -> FROZEN₄(m, Sum_sub₂(xi, s), n, s)
FROZEN₄(m, Sum_constant₁(Left), n, s) -> TERM_SUB₂(m, s)
FROZEN₄(m, Sum_term_var₁(xi), n, s) -> TERM_SUB₂(n, s)
FROZEN₄(m, Sum_term_var₁(xi), n, s) -> TERM_SUB₂(m, s)
FROZEN₄(m, Sum_constant₁(Right), n, s) -> TERM_SUB₂(n, s)

The TRS R consists of the following rules:

Term_sub₂(Case₃(m, xi, n), s) -> Frozen₄(m, Sum_sub₂(xi, s), n, s)
Frozen₄(m, Sum_constant₁(Left), n, s) -> Term_sub₂(m, s)
Frozen₄(m, Sum_constant₁(Right), n, s) -> Term_sub₂(n, s)
Frozen₄(m, Sum_term_var₁(xi), n, s) -> Case₃(Term_sub₂(m, s), xi, Term_sub₂(n, s))
Term_sub₂(Term_app₂(m, n), s) -> Term_app₂(Term_sub₂(m, s), Term_sub₂(n, s))
Term_sub₂(Term_pair₂(m, n), s) -> Term_pair₂(Term_sub₂(m, s), Term_sub₂(n, s))
Term_sub₂(Term_inl₁(m), s) -> Term_inl₁(Term_sub₂(m, s))
Term_sub₂(Term_inr₁(m), s) -> Term_inr₁(Term_sub₂(m, s))
Term_sub₂(Term_var₁(x), Id) -> Term_var₁(x)
Term_sub₂(Term_var₁(x), Cons_usual₃(y, m, s)) -> m
Term_sub₂(Term_var₁(x), Cons_usual₃(y, m, s)) -> Term_sub₂(Term_var₁(x), s)
Term_sub₂(Term_var₁(x), Cons_sum₃(xi, k, s)) -> Term_sub₂(Term_var₁(x), s)
Term_sub₂(Term_sub₂(m, s), t) -> Term_sub₂(m, Concat₂(s, t))
Sum_sub₂(xi, Id) -> Sum_term_var₁(xi)
Sum_sub₂(xi, Cons_sum₃(psi, k, s)) -> Sum_constant₁(k)
Sum_sub₂(xi, Cons_sum₃(psi, k, s)) -> Sum_sub₂(xi, s)
Sum_sub₂(xi, Cons_usual₃(y, m, s)) -> Sum_sub₂(xi, s)
Concat₂(Concat₂(s, t), u) -> Concat₂(s, Concat₂(t, u))
Concat₂(Cons_usual₃(x, m, s), t) -> Cons_usual₃(x, Term_sub₂(m, t), Concat₂(s, t))
Concat₂(Cons_sum₃(xi, k, s), t) -> Cons_sum₃(xi, k, Concat₂(s, t))
Concat₂(Id, s) -> s

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

TERM_SUB₂(Case₃(m, xi, n), s) -> FROZEN₄(m, Sum_sub₂(xi, s), n, s)

The remaining pairs can at least be oriented weakly.

FROZEN₄(m, Sum_constant₁(Left), n, s) -> TERM_SUB₂(m, s)
FROZEN₄(m, Sum_term_var₁(xi), n, s) -> TERM_SUB₂(n, s)
FROZEN₄(m, Sum_term_var₁(xi), n, s) -> TERM_SUB₂(m, s)
FROZEN₄(m, Sum_constant₁(Right), n, s) -> TERM_SUB₂(n, s)

Used ordering: Polynomial interpretation [21]:

POL(Case₃(x₁, x₂, x₃)) = 2 + 2·x₁ + 2·x₃
POL(Cons_sum₃(x₁, x₂, x₃)) = 0
POL(Cons_usual₃(x₁, x₂, x₃)) = 0
POL(FROZEN₄(x₁, x₂, x₃, x₄)) = 2·x₁ + 2·x₃
POL(Id) = 0
POL(Left) = 0
POL(Right) = 0
POL(Sum_constant₁(x₁)) = 0
POL(Sum_sub₂(x₁, x₂)) = 0
POL(Sum_term_var₁(x₁)) = 0
POL(TERM_SUB₂(x₁, x₂)) = 2·x₁

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

                    ↳ QDPOrderProof

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ AND

                                ↳ QDP

                                  ↳ QDPOrderProof

                                    ↳ QDP

                                      ↳ QDPOrderProof

                                        ↳ QDP

                                          ↳ QDPOrderProof

                                            ↳ QDP

                                              ↳ DependencyGraphProof

                                ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

FROZEN₄(m, Sum_constant₁(Left), n, s) -> TERM_SUB₂(m, s)
FROZEN₄(m, Sum_term_var₁(xi), n, s) -> TERM_SUB₂(n, s)
FROZEN₄(m, Sum_term_var₁(xi), n, s) -> TERM_SUB₂(m, s)
FROZEN₄(m, Sum_constant₁(Right), n, s) -> TERM_SUB₂(n, s)

The TRS R consists of the following rules:

Term_sub₂(Case₃(m, xi, n), s) -> Frozen₄(m, Sum_sub₂(xi, s), n, s)
Frozen₄(m, Sum_constant₁(Left), n, s) -> Term_sub₂(m, s)
Frozen₄(m, Sum_constant₁(Right), n, s) -> Term_sub₂(n, s)
Frozen₄(m, Sum_term_var₁(xi), n, s) -> Case₃(Term_sub₂(m, s), xi, Term_sub₂(n, s))
Term_sub₂(Term_app₂(m, n), s) -> Term_app₂(Term_sub₂(m, s), Term_sub₂(n, s))
Term_sub₂(Term_pair₂(m, n), s) -> Term_pair₂(Term_sub₂(m, s), Term_sub₂(n, s))
Term_sub₂(Term_inl₁(m), s) -> Term_inl₁(Term_sub₂(m, s))
Term_sub₂(Term_inr₁(m), s) -> Term_inr₁(Term_sub₂(m, s))
Term_sub₂(Term_var₁(x), Id) -> Term_var₁(x)
Term_sub₂(Term_var₁(x), Cons_usual₃(y, m, s)) -> m
Term_sub₂(Term_var₁(x), Cons_usual₃(y, m, s)) -> Term_sub₂(Term_var₁(x), s)
Term_sub₂(Term_var₁(x), Cons_sum₃(xi, k, s)) -> Term_sub₂(Term_var₁(x), s)
Term_sub₂(Term_sub₂(m, s), t) -> Term_sub₂(m, Concat₂(s, t))
Sum_sub₂(xi, Id) -> Sum_term_var₁(xi)
Sum_sub₂(xi, Cons_sum₃(psi, k, s)) -> Sum_constant₁(k)
Sum_sub₂(xi, Cons_sum₃(psi, k, s)) -> Sum_sub₂(xi, s)
Sum_sub₂(xi, Cons_usual₃(y, m, s)) -> Sum_sub₂(xi, s)
Concat₂(Concat₂(s, t), u) -> Concat₂(s, Concat₂(t, u))
Concat₂(Cons_usual₃(x, m, s), t) -> Cons_usual₃(x, Term_sub₂(m, t), Concat₂(s, t))
Concat₂(Cons_sum₃(xi, k, s), t) -> Cons_sum₃(xi, k, Concat₂(s, t))
Concat₂(Id, s) -> s

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 0 SCCs with 4 less nodes.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

                    ↳ QDPOrderProof

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ AND

                                ↳ QDP

                                ↳ QDP

                                  ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

CONCAT₂(Cons_usual₃(x, m, s), t) -> CONCAT₂(s, t)
CONCAT₂(Concat₂(s, t), u) -> CONCAT₂(s, Concat₂(t, u))
CONCAT₂(Concat₂(s, t), u) -> CONCAT₂(t, u)

The TRS R consists of the following rules:

Term_sub₂(Case₃(m, xi, n), s) -> Frozen₄(m, Sum_sub₂(xi, s), n, s)
Frozen₄(m, Sum_constant₁(Left), n, s) -> Term_sub₂(m, s)
Frozen₄(m, Sum_constant₁(Right), n, s) -> Term_sub₂(n, s)
Frozen₄(m, Sum_term_var₁(xi), n, s) -> Case₃(Term_sub₂(m, s), xi, Term_sub₂(n, s))
Term_sub₂(Term_app₂(m, n), s) -> Term_app₂(Term_sub₂(m, s), Term_sub₂(n, s))
Term_sub₂(Term_pair₂(m, n), s) -> Term_pair₂(Term_sub₂(m, s), Term_sub₂(n, s))
Term_sub₂(Term_inl₁(m), s) -> Term_inl₁(Term_sub₂(m, s))
Term_sub₂(Term_inr₁(m), s) -> Term_inr₁(Term_sub₂(m, s))
Term_sub₂(Term_var₁(x), Id) -> Term_var₁(x)
Term_sub₂(Term_var₁(x), Cons_usual₃(y, m, s)) -> m
Term_sub₂(Term_var₁(x), Cons_usual₃(y, m, s)) -> Term_sub₂(Term_var₁(x), s)
Term_sub₂(Term_var₁(x), Cons_sum₃(xi, k, s)) -> Term_sub₂(Term_var₁(x), s)
Term_sub₂(Term_sub₂(m, s), t) -> Term_sub₂(m, Concat₂(s, t))
Sum_sub₂(xi, Id) -> Sum_term_var₁(xi)
Sum_sub₂(xi, Cons_sum₃(psi, k, s)) -> Sum_constant₁(k)
Sum_sub₂(xi, Cons_sum₃(psi, k, s)) -> Sum_sub₂(xi, s)
Sum_sub₂(xi, Cons_usual₃(y, m, s)) -> Sum_sub₂(xi, s)
Concat₂(Concat₂(s, t), u) -> Concat₂(s, Concat₂(t, u))
Concat₂(Cons_usual₃(x, m, s), t) -> Cons_usual₃(x, Term_sub₂(m, t), Concat₂(s, t))
Concat₂(Cons_sum₃(xi, k, s), t) -> Cons_sum₃(xi, k, Concat₂(s, t))
Concat₂(Id, s) -> s

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

CONCAT₂(Cons_usual₃(x, m, s), t) -> CONCAT₂(s, t)

The remaining pairs can at least be oriented weakly.

CONCAT₂(Concat₂(s, t), u) -> CONCAT₂(s, Concat₂(t, u))
CONCAT₂(Concat₂(s, t), u) -> CONCAT₂(t, u)

Used ordering: Polynomial interpretation [21]:

POL(CONCAT₂(x₁, x₂)) = 2·x₁
POL(Case₃(x₁, x₂, x₃)) = 0
POL(Concat₂(x₁, x₂)) = 2·x₁ + 2·x₂
POL(Cons_sum₃(x₁, x₂, x₃)) = 0
POL(Cons_usual₃(x₁, x₂, x₃)) = 2 + 2·x₃
POL(Frozen₄(x₁, x₂, x₃, x₄)) = 0
POL(Id) = 0
POL(Left) = 0
POL(Right) = 0
POL(Sum_constant₁(x₁)) = 0
POL(Sum_sub₂(x₁, x₂)) = 0
POL(Sum_term_var₁(x₁)) = 0
POL(Term_app₂(x₁, x₂)) = 0
POL(Term_inl₁(x₁)) = 0
POL(Term_inr₁(x₁)) = 0
POL(Term_pair₂(x₁, x₂)) = 0
POL(Term_sub₂(x₁, x₂)) = 0
POL(Term_var₁(x₁)) = 0

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

                    ↳ QDPOrderProof

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ AND

                                ↳ QDP

                                ↳ QDP

                                  ↳ QDPOrderProof

                                    ↳ QDP

                                      ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

CONCAT₂(Concat₂(s, t), u) -> CONCAT₂(s, Concat₂(t, u))
CONCAT₂(Concat₂(s, t), u) -> CONCAT₂(t, u)

The TRS R consists of the following rules:

Term_sub₂(Case₃(m, xi, n), s) -> Frozen₄(m, Sum_sub₂(xi, s), n, s)
Frozen₄(m, Sum_constant₁(Left), n, s) -> Term_sub₂(m, s)
Frozen₄(m, Sum_constant₁(Right), n, s) -> Term_sub₂(n, s)
Frozen₄(m, Sum_term_var₁(xi), n, s) -> Case₃(Term_sub₂(m, s), xi, Term_sub₂(n, s))
Term_sub₂(Term_app₂(m, n), s) -> Term_app₂(Term_sub₂(m, s), Term_sub₂(n, s))
Term_sub₂(Term_pair₂(m, n), s) -> Term_pair₂(Term_sub₂(m, s), Term_sub₂(n, s))
Term_sub₂(Term_inl₁(m), s) -> Term_inl₁(Term_sub₂(m, s))
Term_sub₂(Term_inr₁(m), s) -> Term_inr₁(Term_sub₂(m, s))
Term_sub₂(Term_var₁(x), Id) -> Term_var₁(x)
Term_sub₂(Term_var₁(x), Cons_usual₃(y, m, s)) -> m
Term_sub₂(Term_var₁(x), Cons_usual₃(y, m, s)) -> Term_sub₂(Term_var₁(x), s)
Term_sub₂(Term_var₁(x), Cons_sum₃(xi, k, s)) -> Term_sub₂(Term_var₁(x), s)
Term_sub₂(Term_sub₂(m, s), t) -> Term_sub₂(m, Concat₂(s, t))
Sum_sub₂(xi, Id) -> Sum_term_var₁(xi)
Sum_sub₂(xi, Cons_sum₃(psi, k, s)) -> Sum_constant₁(k)
Sum_sub₂(xi, Cons_sum₃(psi, k, s)) -> Sum_sub₂(xi, s)
Sum_sub₂(xi, Cons_usual₃(y, m, s)) -> Sum_sub₂(xi, s)
Concat₂(Concat₂(s, t), u) -> Concat₂(s, Concat₂(t, u))
Concat₂(Cons_usual₃(x, m, s), t) -> Cons_usual₃(x, Term_sub₂(m, t), Concat₂(s, t))
Concat₂(Cons_sum₃(xi, k, s), t) -> Cons_sum₃(xi, k, Concat₂(s, t))
Concat₂(Id, s) -> s

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

CONCAT₂(Concat₂(s, t), u) -> CONCAT₂(s, Concat₂(t, u))
CONCAT₂(Concat₂(s, t), u) -> CONCAT₂(t, u)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [21]:

POL(CONCAT₂(x₁, x₂)) = 2·x₁
POL(Case₃(x₁, x₂, x₃)) = 0
POL(Concat₂(x₁, x₂)) = 2 + 2·x₁ + 2·x₂
POL(Cons_sum₃(x₁, x₂, x₃)) = 0
POL(Cons_usual₃(x₁, x₂, x₃)) = 0
POL(Frozen₄(x₁, x₂, x₃, x₄)) = 0
POL(Id) = 0
POL(Left) = 0
POL(Right) = 0
POL(Sum_constant₁(x₁)) = 0
POL(Sum_sub₂(x₁, x₂)) = 0
POL(Sum_term_var₁(x₁)) = 0
POL(Term_app₂(x₁, x₂)) = 0
POL(Term_inl₁(x₁)) = 0
POL(Term_inr₁(x₁)) = 0
POL(Term_pair₂(x₁, x₂)) = 0
POL(Term_sub₂(x₁, x₂)) = 0
POL(Term_var₁(x₁)) = 0

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

                    ↳ QDPOrderProof

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ DependencyGraphProof

                              ↳ AND

                                ↳ QDP

                                ↳ QDP

                                  ↳ QDPOrderProof

                                    ↳ QDP

                                      ↳ QDPOrderProof

                                        ↳ QDP

                                          ↳ PisEmptyProof

Q DP problem:
P is empty.
The TRS R consists of the following rules:

Term_sub₂(Case₃(m, xi, n), s) -> Frozen₄(m, Sum_sub₂(xi, s), n, s)
Frozen₄(m, Sum_constant₁(Left), n, s) -> Term_sub₂(m, s)
Frozen₄(m, Sum_constant₁(Right), n, s) -> Term_sub₂(n, s)
Frozen₄(m, Sum_term_var₁(xi), n, s) -> Case₃(Term_sub₂(m, s), xi, Term_sub₂(n, s))
Term_sub₂(Term_app₂(m, n), s) -> Term_app₂(Term_sub₂(m, s), Term_sub₂(n, s))
Term_sub₂(Term_pair₂(m, n), s) -> Term_pair₂(Term_sub₂(m, s), Term_sub₂(n, s))
Term_sub₂(Term_inl₁(m), s) -> Term_inl₁(Term_sub₂(m, s))
Term_sub₂(Term_inr₁(m), s) -> Term_inr₁(Term_sub₂(m, s))
Term_sub₂(Term_var₁(x), Id) -> Term_var₁(x)
Term_sub₂(Term_var₁(x), Cons_usual₃(y, m, s)) -> m
Term_sub₂(Term_var₁(x), Cons_usual₃(y, m, s)) -> Term_sub₂(Term_var₁(x), s)
Term_sub₂(Term_var₁(x), Cons_sum₃(xi, k, s)) -> Term_sub₂(Term_var₁(x), s)
Term_sub₂(Term_sub₂(m, s), t) -> Term_sub₂(m, Concat₂(s, t))
Sum_sub₂(xi, Id) -> Sum_term_var₁(xi)
Sum_sub₂(xi, Cons_sum₃(psi, k, s)) -> Sum_constant₁(k)
Sum_sub₂(xi, Cons_sum₃(psi, k, s)) -> Sum_sub₂(xi, s)
Sum_sub₂(xi, Cons_usual₃(y, m, s)) -> Sum_sub₂(xi, s)
Concat₂(Concat₂(s, t), u) -> Concat₂(s, Concat₂(t, u))
Concat₂(Cons_usual₃(x, m, s), t) -> Cons_usual₃(x, Term_sub₂(m, t), Concat₂(s, t))
Concat₂(Cons_sum₃(xi, k, s), t) -> Cons_sum₃(xi, k, Concat₂(s, t))
Concat₂(Id, s) -> s

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.